Nuprl Lemma : nth_tl_decomp_eq
4,23
postcript
pdf
T
:Type,
m
:
,
L
:
T
List.
m
<||
L
||
nth_tl(
m
;
L
) = (
L
[
m
].nth_tl(1+
m
;
L
))
T
List
latex
Definitions
t
T
,
||
as
||
,
P
Q
,
False
,
A
,
A
B
,
,
x
:
A
.
B
(
x
)
,
nth_tl(
n
;
as
)
,
l
[
i
]
,
Prop
Lemmas
length
wf1
,
nat
wf
,
nth
tl
decomp
,
select
wf
,
nth
tl
wf
origin
T:Type, m:
, L:T List. m<||L|| 
nth_tl(m;L) = (L[m].nth_tl(1+m;L)) 
T List T:Type, m:, L:T List. m<||L|| nth_tl(m;L) = (L[m].nth_tl(1+m;L)) T List T Q
A
Bx:A. B(x)